Nuprl Lemma : rv-identically-distributed_wf
11,40
postcript
pdf
p
:FinProbSpace,
f
:(
),
X
:(
n
:
RandomVariable(
p
;
f
(
n
))).
rv-identically-distributed(
p
;
n
.
f
(
n
);
n
.
X
(
n
))
latex
Definitions
FinProbSpace
,
t
T
,
,
x
:
A
B
(
x
)
,
f
(
a
)
,
x
(
s
)
,
x
:
A
.
B
(
x
)
,
RandomVariable(
p
;
n
)
,
Type
,
,
r
*
s
,
x
.
t
(
x
)
,
(
x
.
F
(
x
)) o
X
,
E(
n
;
F
)
,
s
=
t
,
,
x
:
A
B
(
x
)
,
P
&
Q
,
rv-identically-distributed(
p
;
n
.
f
(
n
);
i
.
X
(
i
))
Lemmas
expectation
wf
,
rv-compose
wf
,
qmul
wf
,
rationals
wf
,
random-variable
wf
,
nat
wf
,
finite-prob-space
wf
origin
p:FinProbSpace, f:(
), X:(n:RandomVariable(p;f(n))).
p:FinProbSpace, f:(), X:(n:RandomVariable(p;f(n))).
TB(x)x:A. B(x)
x. t(x)
B(x)